package fr.upmc.tep.lambda.evaluation.util;

import java.util.ArrayList;

import fr.upmc.tep.lambda.evaluation.exceptions.TypeException;
import fr.upmc.tep.lambda.evaluation.types.LAbstractionNode;
import fr.upmc.tep.lambda.evaluation.types.LApplicationNode;
import fr.upmc.tep.lambda.evaluation.types.LNode;
import fr.upmc.tep.lambda.evaluation.types.LTree;
import fr.upmc.tep.lambda.evaluation.types.LVariableNode;

/**
 * This class handles the different reductions we need to apply in order to
 * evaluate a lambda expression
 * 
 * @author Fabrice Reynaud, Yihan Wang
 *
 */
public class LReduction {

	/**
	 * This function applies a reduction, if needed it calls for an alpha
	 * reduction before calling the beta reduction.
	 * 
	 * @param tree the original tree.
	 * @return the modified tree after a reduction is applied.
	 * @throws TypeException 
	 */
	public LTree reduction(LTree tree) throws TypeException {
			
		LApplicationNode p = (LApplicationNode) tree.getRoot();

		if (p == null) {
			throw new TypeException("The expression is empty.");
		}
		
		LAbstractionNode abs = findFirstLeftAbstracrtion(tree);				
		LApplicationNode app = (LApplicationNode)abs.getParent();
		
		ArrayList<Character> rightVars = findVariables(app.getRight());
		ArrayList<Character> bodyVars = findVariables(abs.getBody());
		ArrayList<Character> availableVars = createAvailableVariables(
														rightVars, bodyVars);
		
		System.out.println("RightVars:" + rightVars.toString());
		System.out.println("BodyVars:" + bodyVars.toString());
		System.out.println("AvailableVars:" + availableVars.toString());
		
		/* Alpha reduction.
		 * Replaces every occurence if a variable in the body appears in the
		 * right branch of the current application.
		 */
		String head;
		for(char c : bodyVars)
			if(rightVars.contains(c)) {
				char r = availableVars.get(0);
				head = abs.getHead();
				abs.setHead(head.replace(c, r));
				replaceAlpha(abs, c, r);
				availableVars.remove(0);
			}
		
		System.out.println("After alpha:" + p.toLambdaExpression());
		
		/* Beta reduction.
		 * Removes the first variable of the head of the current abstraction and
		 * replace every occurence of that variable in the body by the right
		 * branch of the current application.
		 */
		head = abs.getHead();
		char c = head.charAt(0); //TODO if 0 on supprime?!
		if(head.length() == 1) {
			LNode body = abs.getBody();
			app.setLeft(body);
			body.setParent(app);
		}
		else abs.setHead(head.substring(1));
		LNode node = replaceBeta(c, abs.getBody(), app.getRight());
		abs.setBody(node);
		
		LNode oldParent = app.getParent();		
		abs.setParent(oldParent);
		
		if(oldParent != null)
			((LApplicationNode)oldParent).setLeft(abs);
			
		System.out.println("After beta:" + p.toLambdaExpression());
		
		return tree;
	}
	
	/**
	 * This method finds the first Abstraction to the left of the tree. 
	 * @return
	 * @throws TypeException 
	 */
	private LAbstractionNode findFirstLeftAbstracrtion(LTree tree)
			throws TypeException {
		
		LApplicationNode node = (LApplicationNode) tree.getRoot();
		
		while(node.getLeft().getClass().getSimpleName().equals("LApplicationNode"))
			node = (LApplicationNode) node.getLeft();

		if(node.getLeft().getClass().getSimpleName().equals("LAbstractionNode"))
			return (LAbstractionNode) node.getLeft();
		
		else throw new TypeException("Reduction not possible!");
	}	 
	
	/**
	 * This method returns all the names of the variables it finds.
	 * @param node where to start searching.
	 * @return a list of variables.
	 */
	private ArrayList<Character> findVariables(LNode node) {
		ArrayList<Character> list = new ArrayList<Character>();
		String right = node.toLambdaExpression();
		for(char c: right.toCharArray())
			if(!list.contains(c) && c != '(' && c != ')' && c != 'l' && c != '.')
				list.add(c);
		return list;
	}
	
	/**
	 * Finds all the variables that are neither in both arrays.
	 * @param right the variables to the right of an application
	 * @param body the variables of the body of an abstraction
	 * @return the available variables
	 */
	private ArrayList<Character> createAvailableVariables(
						ArrayList<Character> right, ArrayList<Character> body) {
		ArrayList<Character> availableVars = new ArrayList<Character>();
		char[] alpha = {'a', 'b', 'c', 'd', 'e' ,'f', 'g', 'h', 'i', 'j', 'k', 'l', 'm', 'n', 'o', 'p', 'q', 'r', 's', 't', 'u', 'v', 'w', 'x', 'y', 'z'};
		for(char c : alpha)
			if(!right.contains(c) && !body.contains(c))
				availableVars.add(c);
		return availableVars;
	}
	
	/**
	 * Replaces every occurence of 'c' by 'r' in the node.
	 * @param node
	 * @param c
	 * @param r
	 * @return the node with 'c' replaced by 'r'
	 * @throws TypeException 
	 */
	private LNode replaceAlpha(LNode node, char c, char r) throws TypeException {
		
		String name = node.getClass().getSimpleName();
		
		if(name.equals("LApplicationNode")) {
			LApplicationNode app = (LApplicationNode)node;
			LNode left = app.getLeft();
			LNode right = app.getRight();
			replaceAlpha(left, c, r);
			replaceAlpha(right, c, r);
		}
		else if(name.equals("LAbstractionNode")){
			LAbstractionNode abs = (LAbstractionNode)node;
			String head  = abs.getHead();
			LNode body = abs.getBody();
			head.replace(c, r);
			replaceAlpha(body, c, r);
		}
		else if(name.equals("LVariableNode")) {
			LVariableNode var = (LVariableNode)node;
			if(var.getVariable() == c)
				var.setVariable(r);
		}
		else throw new TypeException("Type inconnu:" + name);
		
		return node;
	}
	
	/**
	 * Replaces every occurence of the variable c by the replacement node.
	 * @param c
	 * @param node
	 * @param replacement
	 * @return the modified node
	 * @throws TypeException
	 */
	private LNode replaceBeta(char c, LNode node, LNode replacement) throws TypeException {
		
		String name = node.getClass().getSimpleName();
		
		if(name.equals("LApplicationNode")) {
			LApplicationNode app = (LApplicationNode)node;
			LNode left = app.getLeft();
			LNode right = app.getRight();
			app.setLeft(replaceBeta(c, left, replacement));
			app.setRight(replaceBeta(c, right, replacement));
		}
		else if(name.equals("LAbstractionNode")){
			LAbstractionNode abs = (LAbstractionNode)node;
			LNode body = abs.getBody();
			replaceBeta(c, body, replacement);
		}
		else if(name.equals("LVariableNode")) {
			
			System.out.println("Replacement=" + replacement.toLambdaExpression());
			
			LVariableNode var = (LVariableNode)node;
			if(var.getVariable() == c) {
				replacement.setParent(node.getParent());
				node = replacement;
			}
		}
		else throw new TypeException("Type inconnu:" + name);
		
		return node;
	}
}
